Step of Proof: decidable__assert
9,38
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
decidable
assert
:
(
tt)
(
(
tt))
latex
by ((DNth 1 0)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
tt
C
.
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
btrue
wf
,
assert
wf
,
not
wf
origin